(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 13))
(let ((e3 2))
(let ((e4 4))
(let ((e5 (- v1)))
(let ((e6 (* e3 v1)))
(let ((e7 (/ e4 (- e4))))
(let ((e8 (/ e4 e3)))
(let ((e9 (* e4 e8)))
(let ((e10 (+ v0 v0)))
(let ((e11 (- e10)))
(let ((e12 (/ e3 (- e2))))
(let ((e13 (= e7 e7)))
(let ((e14 (< e11 e11)))
(let ((e15 (= e6 v0)))
(let ((e16 (< e9 e12)))
(let ((e17 (< e6 e12)))
(let ((e18 (< v1 v1)))
(let ((e19 (>= e10 v0)))
(let ((e20 (> v0 e10)))
(let ((e21 (< e11 v1)))
(let ((e22 (> e5 e7)))
(let ((e23 (< e9 e11)))
(let ((e24 (> e8 e12)))
(let ((e25 (ite e18 e10 e9)))
(let ((e26 (ite e24 e10 v0)))
(let ((e27 (ite e13 e10 e11)))
(let ((e28 (ite e17 e7 e9)))
(let ((e29 (ite e23 e6 e7)))
(let ((e30 (ite e22 e12 e10)))
(let ((e31 (ite e21 v1 e29)))
(let ((e32 (ite e19 e8 e7)))
(let ((e33 (ite e16 e5 e28)))
(let ((e34 (ite e16 e5 e25)))
(let ((e35 (ite e21 e28 e31)))
(let ((e36 (ite e23 e25 e5)))
(let ((e37 (ite e23 v1 e36)))
(let ((e38 (ite e18 e32 e37)))
(let ((e39 (ite e14 e28 e25)))
(let ((e40 (ite e19 e29 e9)))
(let ((e41 (ite e13 e29 e39)))
(let ((e42 (ite e20 e36 e12)))
(let ((e43 (ite e17 e37 e26)))
(let ((e44 (ite e14 e39 e43)))
(let ((e45 (ite e21 e7 e37)))
(let ((e46 (ite e15 e36 e26)))
(let ((e47 (<= e10 e38)))
(let ((e48 (>= e36 e34)))
(let ((e49 (<= e45 e35)))
(let ((e50 (<= e33 e46)))
(let ((e51 (> e11 e45)))
(let ((e52 (> e45 e33)))
(let ((e53 (distinct e31 e37)))
(let ((e54 (> e41 e38)))
(let ((e55 (> e45 e33)))
(let ((e56 (< e46 e6)))
(let ((e57 (< e38 e46)))
(let ((e58 (= e29 e34)))
(let ((e59 (= e40 e11)))
(let ((e60 (= e11 e44)))
(let ((e61 (> e44 e12)))
(let ((e62 (distinct e28 e43)))
(let ((e63 (distinct v0 e42)))
(let ((e64 (<= e12 e40)))
(let ((e65 (distinct e28 e41)))
(let ((e66 (distinct e46 e11)))
(let ((e67 (< e25 v1)))
(let ((e68 (> e5 e31)))
(let ((e69 (> v0 e11)))
(let ((e70 (< e34 e26)))
(let ((e71 (<= e30 e38)))
(let ((e72 (< e42 e42)))
(let ((e73 (> e33 e42)))
(let ((e74 (<= e8 e39)))
(let ((e75 (= e37 e41)))
(let ((e76 (< e32 e43)))
(let ((e77 (<= e5 e25)))
(let ((e78 (< e31 e12)))
(let ((e79 (<= e39 e36)))
(let ((e80 (< e36 e40)))
(let ((e81 (<= e43 e30)))
(let ((e82 (>= e37 e39)))
(let ((e83 (<= e33 e31)))
(let ((e84 (distinct e40 e6)))
(let ((e85 (distinct v0 e25)))
(let ((e86 (<= e7 e29)))
(let ((e87 (>= e41 e33)))
(let ((e88 (= e12 e45)))
(let ((e89 (distinct e37 e38)))
(let ((e90 (distinct e8 e36)))
(let ((e91 (distinct e25 e37)))
(let ((e92 (<= e31 e12)))
(let ((e93 (>= e7 e41)))
(let ((e94 (> e44 e34)))
(let ((e95 (<= e42 e26)))
(let ((e96 (distinct e42 e7)))
(let ((e97 (distinct e37 e5)))
(let ((e98 (= e28 v1)))
(let ((e99 (<= e31 e39)))
(let ((e100 (<= e7 e26)))
(let ((e101 (> e39 e42)))
(let ((e102 (= e7 e32)))
(let ((e103 (<= e33 e41)))
(let ((e104 (>= e44 e34)))
(let ((e105 (< e8 e34)))
(let ((e106 (< e36 e9)))
(let ((e107 (>= e40 e12)))
(let ((e108 (distinct e10 e6)))
(let ((e109 (distinct e38 e8)))
(let ((e110 (distinct e30 v1)))
(let ((e111 (distinct e10 e44)))
(let ((e112 (> e34 e7)))
(let ((e113 (< e5 e29)))
(let ((e114 (> e9 e10)))
(let ((e115 (>= e39 e33)))
(let ((e116 (< e31 e39)))
(let ((e117 (<= e25 e10)))
(let ((e118 (>= e35 e11)))
(let ((e119 (<= e44 e35)))
(let ((e120 (<= e34 e31)))
(let ((e121 (distinct e45 e29)))
(let ((e122 (distinct e38 e32)))
(let ((e123 (< e26 e44)))
(let ((e124 (<= v0 e5)))
(let ((e125 (distinct e28 e30)))
(let ((e126 (<= e11 e35)))
(let ((e127 (>= e33 e40)))
(let ((e128 (distinct e41 e29)))
(let ((e129 (distinct e12 e7)))
(let ((e130 (>= e11 e38)))
(let ((e131 (< e34 v0)))
(let ((e132 (distinct e32 e8)))
(let ((e133 (< v1 e10)))
(let ((e134 (> e41 e30)))
(let ((e135 (distinct e37 e11)))
(let ((e136 (distinct e34 e9)))
(let ((e137 (< e35 e36)))
(let ((e138 (> e36 e40)))
(let ((e139 (distinct e41 e8)))
(let ((e140 (>= e7 e42)))
(let ((e141 (distinct e12 e11)))
(let ((e142 (> e38 e27)))
(let ((e143 (xor e138 e129)))
(let ((e144 (= e51 e109)))
(let ((e145 (not e95)))
(let ((e146 (and e80 e69)))
(let ((e147 (xor e14 e131)))
(let ((e148 (= e134 e92)))
(let ((e149 (not e62)))
(let ((e150 (or e22 e114)))
(let ((e151 (= e111 e96)))
(let ((e152 (ite e133 e89 e148)))
(let ((e153 (= e144 e104)))
(let ((e154 (=> e47 e108)))
(let ((e155 (not e71)))
(let ((e156 (not e94)))
(let ((e157 (or e83 e52)))
(let ((e158 (xor e86 e136)))
(let ((e159 (ite e98 e59 e88)))
(let ((e160 (and e19 e78)))
(let ((e161 (= e155 e110)))
(let ((e162 (xor e140 e102)))
(let ((e163 (or e60 e49)))
(let ((e164 (ite e50 e105 e76)))
(let ((e165 (not e142)))
(let ((e166 (=> e101 e147)))
(let ((e167 (and e73 e79)))
(let ((e168 (xor e152 e72)))
(let ((e169 (= e55 e100)))
(let ((e170 (or e124 e57)))
(let ((e171 (or e169 e66)))
(let ((e172 (ite e117 e82 e143)))
(let ((e173 (=> e118 e115)))
(let ((e174 (or e112 e168)))
(let ((e175 (or e157 e70)))
(let ((e176 (not e48)))
(let ((e177 (or e68 e20)))
(let ((e178 (not e128)))
(let ((e179 (= e120 e24)))
(let ((e180 (ite e103 e164 e116)))
(let ((e181 (or e85 e81)))
(let ((e182 (and e91 e13)))
(let ((e183 (not e77)))
(let ((e184 (not e97)))
(let ((e185 (or e63 e181)))
(let ((e186 (and e121 e130)))
(let ((e187 (=> e122 e159)))
(let ((e188 (= e162 e161)))
(let ((e189 (not e166)))
(let ((e190 (and e165 e180)))
(let ((e191 (not e64)))
(let ((e192 (ite e156 e53 e132)))
(let ((e193 (or e167 e21)))
(let ((e194 (or e16 e183)))
(let ((e195 (not e119)))
(let ((e196 (=> e174 e17)))
(let ((e197 (and e107 e149)))
(let ((e198 (ite e163 e192 e90)))
(let ((e199 (=> e170 e145)))
(let ((e200 (and e186 e93)))
(let ((e201 (=> e160 e141)))
(let ((e202 (xor e106 e196)))
(let ((e203 (=> e184 e182)))
(let ((e204 (=> e18 e151)))
(let ((e205 (=> e84 e195)))
(let ((e206 (=> e176 e58)))
(let ((e207 (xor e200 e190)))
(let ((e208 (ite e178 e113 e139)))
(let ((e209 (not e204)))
(let ((e210 (=> e126 e203)))
(let ((e211 (xor e74 e185)))
(let ((e212 (not e87)))
(let ((e213 (and e208 e123)))
(let ((e214 (and e54 e158)))
(let ((e215 (=> e194 e187)))
(let ((e216 (not e179)))
(let ((e217 (=> e171 e65)))
(let ((e218 (and e75 e191)))
(let ((e219 (xor e216 e193)))
(let ((e220 (xor e127 e173)))
(let ((e221 (not e172)))
(let ((e222 (=> e146 e221)))
(let ((e223 (= e175 e197)))
(let ((e224 (or e153 e99)))
(let ((e225 (ite e125 e137 e188)))
(let ((e226 (= e225 e209)))
(let ((e227 (=> e205 e198)))
(let ((e228 (not e23)))
(let ((e229 (xor e213 e201)))
(let ((e230 (=> e189 e217)))
(let ((e231 (or e207 e228)))
(let ((e232 (= e224 e227)))
(let ((e233 (= e226 e218)))
(let ((e234 (= e219 e223)))
(let ((e235 (= e56 e210)))
(let ((e236 (= e154 e15)))
(let ((e237 (and e177 e67)))
(let ((e238 (or e199 e237)))
(let ((e239 (ite e220 e202 e214)))
(let ((e240 (=> e238 e238)))
(let ((e241 (=> e222 e231)))
(let ((e242 (xor e233 e150)))
(let ((e243 (xor e234 e232)))
(let ((e244 (= e243 e243)))
(let ((e245 (not e244)))
(let ((e246 (=> e135 e245)))
(let ((e247 (not e215)))
(let ((e248 (and e242 e241)))
(let ((e249 (= e235 e212)))
(let ((e250 (= e240 e236)))
(let ((e251 (=> e247 e250)))
(let ((e252 (xor e239 e61)))
(let ((e253 (=> e252 e206)))
(let ((e254 (= e249 e229)))
(let ((e255 (and e230 e230)))
(let ((e256 (= e253 e248)))
(let ((e257 (and e246 e211)))
(let ((e258 (ite e256 e254 e254)))
(let ((e259 (ite e255 e251 e251)))
(let ((e260 (or e259 e258)))
(let ((e261 (=> e260 e260)))
(let ((e262 (= e257 e261)))
e262
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
